Nuprl Definition : hgrp_car
13,42
postcript
pdf
|
g
|
== {
x
:|
g
|| e
x
}
latex
clarification:
|
g
|
== {
x
:|
g
|| (e
g
)
g
x
}
latex
Up
groups
1
Wellformedness Lemmas
hgrp
car
wf
Definitions
|
g
|
,
a
b
,
e
origin
== {x:|g|| e 
x}
== {x:|g|| (eg) g x} == {x:|g|| e x}
== {x:|g|| (eg) g x} b